$\forall$$E$, $T$, $X_{1}$, $X_{2}$:Type, ${\it info}$:($E$$\rightarrow$(Id$\times$$X_{1}$+(IdLnk$\times$$E$)$\times$$X_{2}$)), $e$:$E$, $f$:(Id$\rightarrow$$T$), $g$:(IdLnk$\rightarrow$$E$$\rightarrow$$T$).
\\[0ex]ecase1($e$;${\it info}$;$i$.$f$($i$);$l$,${\it e'}$.$g$($l$,${\it e'}$)) $\in$ $T$